Nuprl Lemma : map-wf2
0,22
postcript
pdf
A
,
B
:Type,
L
:
A
List,
f
:({
x
:
A
| (
x
L
) }
B
). map(
f
;
L
)
B
List
latex
Definitions
t
T
,
x
:
A
.
B
(
x
)
,
(
x
l
)
,
S
T
,
S
T
,
Prop
,
{
T
}
,
P
Q
,
P
Q
,
P
Q
,
P
&
Q
,
P
Q
Lemmas
cons
member
,
l
member
wf
origin
A, B:Type, L:A List, f:({x:A| (x 
L) }
B). map(f;L) B List A, B:Type, L:A List, f:({x:A| (x L) }B). map(f;L) B List Tx:A. B(x) l)
T
T
Q
Q
Q Q